T:Type, eq:EqDecider(T), f, g, h:x:T fp Type.
f || g
 h || f
 h || g
 {g  h  f  g & f  h  f  g & h  g  h  f  g & h  f  h  f  g} 

latex

Definitions	x:A. B(x), P  Q, t  T, x. t(x), {T}, P & Q, f  g, A c B, P  Q, P  Q, P  Q, , Top, if b then t else f fi , tt, ff, x(s), f || g, , Unit, A, False,
Lemmas	fpf-compatible wf, fpf wf, deq wf, iff transitivity, assert wf, fpf-dom wf, fpf-join wf, fpf-join-dom2, or functionality wrt iff, fpf-join-ap-sq, bool wf, eqtt to assert, bnot wf, not wf, eqff to assert, assert of bnot, fpf-ap wf, fpf-trivial-subtype-top, top wf